\documentclass{article}
\usepackage{graphicx}
\usepackage[french]{babel}
\usepackage[utf8]{inputenc}
\usepackage[left=3cm, right=3cm, top=2.5cm, bottom=2.5cm]{geometry}
\usepackage[vlined,lined,linesnumbered,boxed,french]{algorithm2e}
\usepackage{amsmath,amsfonts}

\DeclareMathSizes{10}{8}{6}{4}

\author{Thibaud Lambert, Clement Pinet}
\title{Contrôle continu: logique et preuve de programmes}
\date{Mai 2012}

\begin{document}
\maketitle

\section{Nombre premier}
\subsection{Exercice 1}

\subsubsection{Pré-conditions et post-conditions}
La fonction prime retourne un booléen indiquant si l'entier passé en
paramètre est premier. La notion de nombre premier étant défini sur
$\mathbb{N}$, l'entier passé en paramètre doit être un entier naturel.
La valeur de retour doit être 0 si n n'est pas premier et n'importe
quelle valeur différente de 0 si n est premier.\\ Sa spécification est
(r représente la valeur de retour):\\

\begin{description}
\item[pré-condition:] $ n \in \mathbb{N}$\\
\item[post-condition:] $ (r = 0) \Leftrightarrow ((\exists k \in \mathbb{N} \setminus \{n,1\},~k \mid n) \lor n=0 \lor n=1$ \\
\end{description}



\subsubsection{Variant et terminaison}
On prend comme variant : $ isqrt(n)-i + 1 $ avec $isqrt(n) \in
\mathbb{N}$ et $i \in \mathbb{N}$.\\ 

Comme on a : $ i \leq isqrt(n) $ alors $isqrt(n) - i +1 \geq 0$.\\ 
On sait que $ i=2$ à la premiére itération et que $ n \geq 3$ donc on
a bien $ isqrt(n)-i + 1 \in \mathbb{N}$ avant la première itération de
la boucle.\\ 
On suppose maitenant que $isqrt(n) - i + 1 \in
\mathbb{N}$ alors après exécution de $i := i+1$
on a : $isqrt(n) - (i+1) +1 \in \mathbb{N}$ donc notre variant reste
bien dans $\mathbb{N}$.\\

Appelons $X$ la valeur de $isqrt(n) - i + 1$ avant exécution du corps de la boucle.\\
$isqrt(n) - i + 1  = X$ et $ i \leq isqrt(n) $ \\
$isqrt(n) - (i+1) + 1  = isqrt(n) - i$\\
$isqrt(n) - (i+1) + 1 \leq X$\\
Donc $isqrt(n) - i + 1$ est strictement décroissante.\\

$(\mathbb{N},\leq)$ est un ensemble bien fondé. $isqrt(n) - i +1$ est
un terme décroissant pour $\leq$ et à valeur dans $\mathbb{N}$. Donc
$isqrt(n) - i +1$ converge et donc notre programme termine.\\

\subsubsection{Invariant et correction}

On prend comme invariant : $\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)$
Condition d'arret de la boucle:\\
\begin{itemize}
  \item $(n\%i==0)$ : i est un diviseur de n, donc n n'est pas premier. Alors l'algorithme retourne 0\\
  \item $i>isqrt(n)$ : d'après l'invariant de boucle il n'existe pas de diviseur de n plus petit que i. De ce fait il est impossible qu'il existe un diviseur plus grand (sinon il devrait être multiplié par un entier inferieur) donc n est premier. Dans ce cas, l'algorithme retourne $n\%i$ (dans ce cas $n\%i != 0$)\\
\end{itemize}

\subsection{Exercice 2}

\subsubsection{Annotation et logique de Hoare}

Pour la suite de cette partie, on note :\\
$\{P\} = \{n \in \mathbb{N} \}$ \\
$\{R\} = \{(r = 0) \Leftrightarrow (\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1 \}$\\

Pour des raisons de lisibilité, l'arbre de preuve est divisé en plusieurs partie.\\

\medskip
On commence donc avec le triplet de Hoare formé par notre
pre\-condition, notre post\-condition et notre programme. On commence
par appliquer la règle de la conditionnelle.
\begin{displaymath}
\frac{\{n \in \mathbb{N} \land n < 2\} r:=0 \{R\} 
~~~~~~~~~~~~~~~~~~~~ 
\{n \in \mathbb{N} \land n \geq 2\} A \{R\}}{
\frac{\{P\}\text{ if } n < 2 \text{ then }r:=0 \text{ else } A \text{ end } \{R\}}
{\{P\} prime \{R\}}}cond
\end{displaymath}
Ici, prime représente l'ensemble du code de notre programme, A est le code exécuté dans le else du premier if.\\



\medskip
\medskip
\medskip
Il faut prouver la validité des 2 nouveaux triplets. On s'intéresse
d'abord à celui de gauche. En utilisant, une régle de conséquence et
une régle d'affectation on arrive donc à montrer qu'il est valide à
condition que l'obligation de preuve générée est valide.
\begin{displaymath}
\frac{O_1
~~~~~
\overline{\{(\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1 \}~r:=0~\{R\}}^{aff}
}{\{n \in \mathbb{N} \land n < 2\}~r:=0~\{R\}}cons
\end{displaymath}
Avec $\{ O_1 \} = \{ (n \in \mathbb{N} \land n < 2) \Rightarrow ((\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1) \}$\\



\medskip
\medskip
\medskip
Pour celui de droite, On applique la régle de la conditionnelle. On
obtient alors deux nouveaux triplets à prouver.
\begin{displaymath}
\frac
{\{n \in \mathbb{N} \land n \geq 2\ \land n=2\}~r:=1~\{R\} 
~~~~~~~~~~~~~~~~~~~~~~
\{n \in \mathbb{N} \land n \geq 2\ \land \neg(n=2)\}~B~\{R\}}
{\{n \in \mathbb{N} \land n \geq 2\}\text{ if } n == 2 \text{ then }r:=1 \text{ else } B \text{ end } \{R\}}cond
\end{displaymath}
B représente le code du else du second if.\\



\medskip
\medskip
\medskip
Pour prouver la validité de celui de droite, on applique une régle de
consequence qui nous génère deux nouvelles obligations de preuves, et
ensuite une règle d'affectation.
\begin{displaymath}
\frac
{O_2 
~~~~~~
\overline{\{(\forall k \in \mathbb{N} \setminus \{n,1\}, \neg(k \mid n)) \land n\ne0 \land n\ne1~r:=1~\{(r \ne 0) \Leftrightarrow (\forall k \in \mathbb{N} \setminus \{n,1\}, \neg(k \mid n)) \land n\ne0 \land n\ne1 \}}^{aff}
~~~~~~
O_3}
{\{n \in \mathbb{N} \land n \geq 2\ \land n=2\}~r:=1~\{R\}}cond
\end{displaymath}
Avec $\{O_2\} = \{(n \in \mathbb{N} \land n \geq 2\ \land n=2) \Rightarrow ((\forall k \in \mathbb{N} \setminus \{n,1\}, \neg(k \mid n)) \land n\ne0 \land n\ne1)\}$\\
$\{O_3\} = \{((r \ne 0) \Leftrightarrow (\forall k \in \mathbb{N} \setminus \{n,1\}, \neg(k \mid n)) \land n\ne0 \land n\ne1) \Rightarrow  R \}$\\



\medskip
\medskip
\medskip
Pour le triplet de gauche, on applique une règle de séquence pour
découper notre triplet en trois.\\
Où $ I = \forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)$\\
\begin{displaymath}
\frac
{\{n \in \mathbb{N} \land n \geq 2\ \land \neg(n=2)\}~i:=2~\{I\} 
~~~~~~
\{I\} \text{ while } C \text{ do }~i:=i+1~\text{ end } \{I \land \neg C \}
~~~~~~
\{I \land \neg C \}~r:=(n\%i \ne 0)~\{R\}} 
{\{n \in \mathbb{N} \land n \geq 2\ \land \neg(n=2)\}~i:=2;~ \text{ while } C \text{ do }~i:=i+1~\text{ end };~r:= (n\%i \ne 0)~\{R\}}sequ
\end{displaymath}
C est la condition du while: $(i \leq isqrt(n)) \land ( n\%i \ne 0))$\\



\medskip
\medskip
\medskip
Le triplet de droite se prouve en appliquant une règle de conséquence
qui génère une nouvelle obligation de preuve et ensuite une règle
d'affectation.
\begin{displaymath}
\frac
{O_4
~~~~~~
\overline{\forall k \in \mathbb{N}, 2 \leq k < 2 \Rightarrow \neg (k \mid n)~i:=2~\{I\}}^{aff}}
{\{n \in \mathbb{N} \land n \geq 2\ \land \neg(n=2)\}~i:=2~\{I\}}
\end{displaymath}
Avec $ \{O_4\} = \{n \in \mathbb{N} \land n \geq 2\ \land \neg(n=2)\} \Rightarrow \forall k \in \mathbb{N}, 2 \leq k < 2 \Rightarrow \neg (k \mid n)$\\



\medskip
\medskip
\medskip
Le triplet du milieu constitue la boucle while de notre programme. On
applique donc la règle de while puis une règle de conséquence et enfin
une règle d'affectation. Une autre obligation de preuves a été généré.
\begin{displaymath}
\frac
{O_5
~~~~~~
\overline{\{ \forall k \in \mathbb{N}, 2 \leq k < i+1 \Rightarrow \neg (k \mid n)\}~i:=i+1~\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)}^{aff}}
{\frac
{\{I \land C \}~i:=i+1~\{I\}}
{\{I\} \text{ while } C \text{ do }~i:=i+1~\text{ end } \{I \land \neg C \}}while}cons
\end{displaymath}
Avec $\{O_5\} = \{((\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)) \land (i \leq isqrt(n)) \land ( n\%i \ne 0)) \Rightarrow (\forall k \in \mathbb{N}, 2 \leq k < i+1 \Rightarrow \neg (k \mid n))\}$\\



\medskip
\medskip
\medskip
Pour le troisième triplet, on utilise une règle de conséquence suivi
d'une régle d'affectation. Une dernière obligation de preuve a été
générée.
\begin{displaymath}
\frac
{ O_6
~~~~~~
\overline{\{((n\%i \ne 0) = 0) \Leftrightarrow (\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1 \} r:= (n\%i \ne 0) \{R\}}^{aff}}
{\{I \land \neg C \}~r:= (n\%i \ne 0)~\{R\}}cons
\end{displaymath}
Avec $ \{O_6\} = \{ (I \land \neg C) \Rightarrow (((n\%i \ne 0) = 0) \Leftrightarrow (\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1 )\}$\\



\medskip
\medskip
\medskip
Nous avons généré les obligations de preuves, il suffit de prouver
leur validité pour prouver la validité de notre programme.\\

%% \begin{algorithm}[H]
%%   \textbf{prime}
%%   \KwData integer n
%%   \KwResult boolean
%%   integer i\\
%%   boolean r\\
%%   \eIf{$n < 2$}
%%       {$r \leftarrow 0$\\}
%%       {\eIf{$n==2$}
%%         {$r \leftarrow 1$}
%%         {$i \leftarrow 2; $
%%           \While{ $( ( i \leq isqrt(n) ) and ( n\%i \ne 0 ) )$}{
%%             $i \leftarrow i + 1$}
%%       $r \leftarrow ( n\%i \ne 0 )$}}
%%   return r
%% \end{algorithm}


\subsubsection{Obligations de preuve}

Nous avons donc généré 6 obligations de preuves:

$\{ O_1 \} = \{ (n \in \mathbb{N} \land n < 2) \Rightarrow ((\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1) \}$\\

$\{O_2\} = \{(n \in \mathbb{N} \land n \geq 2\ \land n=2) \Rightarrow ((\forall k \in \mathbb{N} \setminus \{n,1\}, \neg(k \mid n)) \land n\ne0 \land n\ne1 )\}$\\

$\{O_3\} = \{((r \ne 0) \Leftrightarrow (\forall k \in \mathbb{N} \setminus \{n,1\}, \neg(k \mid n)) \land n\ne0 \land n\ne1) \Rightarrow  ((r = 0) \Leftrightarrow (\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1 ) \}$\\

$ \{O_4\} = \{n \in \mathbb{N} \land n \geq 2\ \land \neg(n=2)\} \Rightarrow \forall k \in \mathbb{N}, 2 \leq k < 2 \Rightarrow \neg (k \mid n)$\\

$\{O_5\} = \{((\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)) \land (i \leq isqrt(n)) \land ( n\%i \ne 0)) \Rightarrow (\forall k \in \mathbb{N}, 2 \leq k < i+1 \Rightarrow \neg (k \mid n))\}$\\

$ \{O_6\} = \{ (\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n) \land \neg (i \leq isqrt(n)) \land ( n\%i \ne 0))) \Rightarrow (((n\%i \ne 0) = 0) \Leftrightarrow (\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1 )\}$\\

Pour l'obligation $O_1$, on a:\\
$(n \in \mathbb{N} \land n < 2) \Rightarrow n=0 \lor n=1$ \\
$n=0 \lor n=1 \Rightarrow ((\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1)$\\
Donc $O_1$ est valide.\\

Pour $O_2$, on peut écrire:\\
$(n \in \mathbb{N} \land n \geq 2\ \land n=2) \Rightarrow n=2$\\
$ n=2 \Rightarrow ((\forall k \in \mathbb{N} \setminus \{n,1\}, \neg(k \mid n)) \land n\ne0 \land n\ne1)$\\

L'obligation $O_3$ est une simple contraposée.\\

Considérons maintenant l'obligation 4.
Comme $2 \leq k < 2$ est faux $\forall k \in \mathbb{N}$ l'implication suivante est vraie pour n'importe quel n.\\
$\forall k \in \mathbb{N}, 2 \leq k < 2 \Rightarrow \neg (k \mid n)$\\
Et donc l'obligation $O_4$ est valide car la deuxième partie de l'implication est tout le temps vraie.\\

Pour l'obligation $0_5$, on a:
\\ $((\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)) \land (i \leq isqrt(n)) \land ( n\%i \ne 0))$\\ 
On sait donc que $n$ n'admet pas de diviseur strictement
inférieure à $i$ et que $i$ ne divise pas $n$. Donc on n n'admet pas de
diviseur strictement inférieure à $i + 1$. Ainsi on a prouvé la validité
de l'obligation $O_5$.\\

Et finalement l'obligation $O_6$, on peut avoir l'une des deux
conditions suivantes vraies il faut alors montrer dans chaque cas que
l'implication est vraie aussi.\\
Si on a :
$(\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)) \land (i > isqrt(n))$\\
Alors $n$ n'admet pas de diviseurs inférieurs à $isqrt(n)$ donc comme $i > isqrt(n)$, $i$ ne divise pas non plus $n$. On a bien $(n\%i \ne 0)$. Et donc la formule $((n\%i \ne 0) = 0)$ est fausse. La deuxième partie de l'équivalence est exatement la négation de $\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n)$. On a donc faux équivalent à faux, c'est donc vraie. Donc l'implication est vraie dans ce cas.\\

Pour le deuxième cas, si on a:
$\forall k \in \mathbb{N}, 2 \leq k < i \Rightarrow \neg (k \mid n) \land ( n\%i = 0))$\\
Alors $( n\%i = 0))$ signifie que n admet un diviseur autre que 1 et lui même donc $(\exists k \in \mathbb{N} \setminus \{n,1\}, k \mid n) \lor n=0 \lor n=1 )$ est vraie. De même, $((n\%i \ne 0) = 0)$ est vraie. donc l'équivalence est vraie. Et donc l'implication aussi.

\end{document}
